\begin{tabbing}
$\forall$${\it es}$:ES, $l_{1}$, $l_{2}$:IdLnk, ${\it tg}_{1}$, ${\it tg}_{2}$:Id.
\\[0ex]es{-}responsive(${\it es}$;$l_{1}$;${\it tg}_{1}$;$l_{2}$;${\it tg}_{2}$)
\\[0ex]$\Rightarrow$ ($\exists$\=$f$:\{$e$:E$\mid$ kind($e$) = rcv($l_{1}$,${\it tg}_{1}$) $\in$ Knd\} $\rightarrow$\{$e$:E$\mid$ kind($e$) = rcv($l_{2}$,${\it tg}_{2}$) $\in$ Knd\} \+
\\[0ex]Bij(\{$e$:E$\mid$ kind($e$) = rcv($l_{1}$,${\it tg}_{1}$) $\in$ Knd\} ;\{$e$:E$\mid$ kind($e$) = rcv($l_{2}$,${\it tg}_{2}$) $\in$ Knd\} ;$f$))
\-
\end{tabbing}